#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"

int foo(int a, int b) {
	int c=klee_change(1,0);
	if (a<0) {
		for (int i=1;i<=klee_change(b,a);++i)
			c+=klee_change(a,b);
	}
	return c;
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  if (x>=5 && x<7)
	return foo(x,5);
  return 0;
}
